DECLARE INDVAR X Y Z;
DECLARE PREDCONST F 1;
ASSUME ¬∃X.∀Y.(F(X)⊃F(Y));
UNIFY ∀X.∃Y.(F(X)∧¬F(Y)) 1;
∀E 2 X;
∃E 3 Y;
∀E 2 Y;
$